Termination of the following Term Rewriting System could be proven:
Context-sensitive rewrite system:
The TRS R consists of the following rules:
f(a, b, X) → f(X, X, X)
c → a
c → b
The replacement map contains the following entries:f: {3}
a: empty set
b: empty set
c: empty set
↳ CSR
↳ CSDependencyPairsProof
Context-sensitive rewrite system:
The TRS R consists of the following rules:
f(a, b, X) → f(X, X, X)
c → a
c → b
The replacement map contains the following entries:f: {3}
a: empty set
b: empty set
c: empty set
Using Improved CS-DPs we result in the following initial Q-CSDP problem.
↳ CSR
↳ CSDependencyPairsProof
↳ QCSDP
↳ QCSDependencyGraphProof
Q-restricted context-sensitive dependency pair problem:
For all symbols f in {f, F} we have µ(f) = {3}.
The ordinary context-sensitive dependency pairs DPo are:
F(a, b, X) → F(X, X, X)
The TRS R consists of the following rules:
f(a, b, X) → f(X, X, X)
c → a
c → b
Q is empty.
The approximation of the Context-Sensitive Dependency Graph contains 0 SCCs.
The rules F(a, b, z0) → F(z0, z0, z0) and F(a, b, x0) → F(x0, x0, x0) form no chain, because ECapµ(F(z0, z0, z0)) = F(z0, z0, x_1) does not unify with F(a, b, x0).